%% @author Robert Ahrens <mindangels@yahoo.com>
-module(prun).
-behaviour(backtrack).
-export([
         unify/3, 
         unify/4,
         run_query/4,
         test_db/0
        ]).

-compile(export_all).

-define(is_primitive(X), (is_atom(X) orelse is_number(X))).


%% TODO: Okay, need to change the way we do variable bindings to
%%   1) store a separate list of "resolutions" 
%%          [{Var, ResList}]
%%      and when we bind any Var in that list, solve all its
%% resolutions.  (eg. we might also have
%%          [{Var, {res, {ok, Var}, Var2}}]
%% and we have to know that when we bind Var2 to {ok, foo} we need
%% to go through and bind Var to foo.
%%     NOTE: The above format is not right for this, just a sketch.
%%
%%   2) Need to bind arguments at rule-call time and then pass
%% in *only* those bindings.  Then reconcile binding lists at the
%% end of a rule-call.  Need some kind of collapsing logic here.
%% That way we get scoping "for free" (ie. as part of correctness)
%% and don't have to tag all variables with a specific Scope
%% reference.  It just falls out of the implementation.
%%
%%   3) Do away with "fact" as a type.  "facts" are just rules
%% with zero dependent clauses, and since
%%    reconcile_rule(Clauses=[], Bindings, DB) -> {ok, Bindings, DB}
%% then we don't need a separate technology to handle this case.
%%     It also allows us to graciously handle a case like
%%
%% likes(sarah, cheese).
%% likes(zoa, mice).
%% likes(zoa, X) -> likes(sarah, X).
%%
%% where we mingle declarative facts with conditional ones within
%% the same rule.  That would be a p.i.t.a. with the separated 
%% implementation.
%%
%%   4) One day, for performance, we will want to call length(Args)
%% on the arg-lists for all rules and functions and store it in
%% the data-structure that represents them.  That will save
%% potentially *a lot* of time over recursively trying to unify
%% arbitrary arg-lists that aren't going to reconcile.  Don't know
%% how early we need to do this though.
%%


%% Erlang version of a prolog runtime.
get_binding(VarName, Bindings) ->
    case proplists:lookup(VarName, Bindings) of
        {VarName, Val} ->
            {bound, Val};
        none ->
            none
    end.


lookupdb(QName, Database) ->
    [{Type, Attrs} || {Type, Name, Attrs} <- Database, Name == QName].






%% Attempt to bind RuleArgs from ContextBindings.  Return
%% {ok, InitialBindings, BindMap} where InitialBindings is
%% the binding set for the rule's evaluation and BindMap
%% is the instruction set for propagating the final bindings
%% of a successful rule back out to ContextBindings.
%%extract_bindings([Arg1|ArgRest], ContextBindings) ->
%%    case unify(Arg


value_search([{fact, Attrs}|Rest], Args, Bindings, Database) ->
    case unify(Attrs, Args, Bindings, Database) of
        {ok, NewBindings} ->
            {ok, NewBindings, Database};
        fail ->
            value_search(Rest, Args, Bindings, Database)
    end;
value_search([{rule, {RuleArgs, RuleCases}}|Rest], Args, Bindings, Database) ->
    %% TODO: Should the next line really be
    %% unify(RuleArgs, Args, [], Database) and then do
    %% {ok, Bind3 ++ Bindings, DB2} later on?  I ask because this
    %% affects *scoping* and will ensure that we don't have variables from
    %% outer (or other) scopes clobbering us here at this time.
    case unify(Args, RuleArgs, Bindings, Database) of
        {ok, Bind2} ->
            io:format("Bound rule with bindings ~p, cases = ~p~n", [Bind2, RuleCases]),
            case try_rule(RuleCases, Bind2, Database) of
                {ok, Bind3, DB2} ->
                    {ok, Bind3, DB2};
                fail ->
                    value_search(Rest, Args, Bindings, Database)
            end;
        fail ->
            io:format("Failed to bind ruleargs ~p to args ~p~n", [RuleArgs, Args]),
            value_search(Rest, Args, Bindings, Database)
    end;
value_search([], _, _, _) ->
    fail.


%% @note: value_search({fact, Attrs}) ~= value_search({rule, Attrs, []})
%% Maybe we can collapse the two into one representation?
try_rule([{QName, QArgs}|Rest], Bindings, DB) ->
    case run_query(QName, QArgs, Bindings, DB) of
        {ok, NewBindings, NewDB} ->
            try_rule(Rest, NewBindings, NewDB);
        fail ->
            fail
    end;
try_rule([], Bindings, DB) ->
    {ok, Bindings, DB}.


unify(X, Y, DB) ->
    unify(X, Y, [], DB).


run_query(QName, Args, Bindings, Database) ->
    MatchList = lookupdb(QName, Database),
    value_search(MatchList, Args, Bindings, Database).


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%
%%  2nd Attempt
%%


call_rule(RuleName, ArgSchema, Bindings, Database) ->
    %% TODO: Damnit, support arg evaluation before passing
    %% args into the rule....
    case reify_args(ArgSchema, Bindings, DB) of
        {ok, InitialArgs, Bind2, DB2} ->
            ClauseList = lookupdb(RuleName, Database),
            try_clauses(ClauseList, InitialArgs, Bind2, DB2);
        fail ->
            fail
    end.


%% Iterate over Schema and bind in each member.  Either return
%% {ok, InitialArgs, FinalBindings, FinalDB} if successful
%% or else fail.
reify_args(Schema, Bindings, DB) ->
    throw(not_implemented_yet).


%% NOTE: This approach isn't tail recursive and therefore isn't
%% scaleable as a language implementation.  But I am trying to
%% be correct first and then worry about 
try_clauses([], ArgVals, OuterBindings, DB) ->
    fail;
try_clauses([{rule, {ArgSpec, ExprList}}|ORules], ArgVals, OuterBindings, DB) ->
    %%?NOTE: Deliberately start with no "extra" bindings 
    %% other than what's passed in as ArgVals.
    case unify(ArgSpec, ArgVals, [], DB) of
        {ok, InitialBindings, DB2} ->
            case try_expressions(ExprList, InitialBindings, DB2) of
                {ok, Value, FinalBindings, DB3} ->
                    {ok, Value, reconcile_bindings(FinalBindings, OuterBindings), DB3};
                fail ->
                    try_clauses(ORules, ArgVals, OuterBindings, DB)
            end;
        fail ->
            try_clauses(ORules, ArgVals, OuterBindings, DB)
    end.


%% Reconcile InnerBindings (result of walking the expression list)
%% with OuterBindings (the calling context) to produce an updated
%% context to be handed on to the next call.
reconcile_bindings(InnerBindings, OuterBindings) ->
    throw(not_yet_implemented).


try_expressions([], Bindings, DB) ->
    {ok, null, Bindings, DB};
try_expressions([Expr|Rest], Bindings, DB) ->
    case try_expr(Expr, Bindings, DB) of
        {ok, Value, Bind2, DB2} ->
            case Rest of
                [] -> {ok, Value, Bind2, DB2};
                _ -> try_expressions(Rest, Bind2, DB2)
            end;
        fail ->
            fail
    end.


%% @spec try_expr(Expr, Bindings, DB) -> {ok, Value, Bind2, DB2} | fail
%%try_expr({term, T}, Bindings, DB) ->
%%    unify(T, Bindings, DB);
try_expr({rule, {Name, ArgSchema}}, Bindings, DB) ->
    call_rule(Name, ArgSchema, Bindings, DB);
try_expr({erlang, {M, F, AList}}, Bindings, DB) ->
    case reify_args(Alist, Bindings, DB) of
        {ok, ExprArgs, Bind2, DB2} ->
            {ok, apply(M, F, ExprArgs), Bind2, DB};
        fail ->
            fail
    end;
try_expr({unify, SubEx1, SubEx2}, Bindings, DB) ->
    case try_expr(SubEx1, Bindings, DB) of
        {ok, Val1, Bind2, DB2} ->
            case try_expr(SubEx2, Bind2, DB2) of
                {ok, Val2, Bind3, DB3} ->
                    unify(Val1, Val2, Bind3, DB3);
                fail ->
                    fail
            end;
        fail ->
            fail
    end;
try_expr(NakedTerm, Bindings, DB) ->
    unify(NakedTerm, Bindings, DB).


%%
%%  end 2nd attempt
%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


%% @note: Ok, here's the deal!  ONLY unbound variables should
%% be built on pointers to other variables.  So if I bind X = Y
%% and Y is already bound {'Y', foo} then Y remains only bound
%% to foo, and {'X', foo} is also added.  Only in the case where
%% two unbound variables bind do we add insert the loop here
%% and in that case we try to catch it whenever another variable
%% is bound to either of them.
%%     Before you start coding again, think through how much
%% sense this makes.  Also, get a good handle on the difference
%% between the LHS and the RHS of a bind.  Is there one?  And, 
%% if so, what is it?
%%     More generally, what is the best representation of a cluster
%% of variables all bound to one another?  And how is this best
%% applied in the case of subtrees?
bind(X, {var, Y}, Bindings) ->
    throw(working_here);
bind(X, Y, Bindings) ->
    {XVarBindings, OtherBindings} = 
        lists:splitwith(
          fun ({M, {var, _}}) when M == X -> true;
              (_) -> false
          end,
          Bindings
         ),
    do_bind(XVarBindings, Y, [{X, Y} | OtherBindings]).


do_bind([{var, V}|Rest], Val, Bindings) ->
    case unify({var, V}, Val, Bindings) of
        {ok, NewBindings} ->
            do_bind(Rest, Val, NewBindings);
        fail ->
            fail
    end;
do_bind([], _, Bindings) ->
    {ok, Bindings}.
                                               


%% @spec unify(pterm(), pterm(), bindings(), database()) -> {ok, bindings(), database()} | fail
unify({var, X}, {var, Y}, Bindings, DB) ->
    case {get_binding(X, Bindings), get_binding(Y, Bindings)} of
        {none, none} ->
            {ok, [{X, {var, Y}}, {Y, {var, X}}|Bindings]};
        {none, {bound, BindY}} ->
            {ok, [{X, BindY}|Bindings]};
        {{bound, BindX}, none} ->
            {ok, [{Y, BindX}|Bindings]};
        {{bound, BindX}, {bound, BindY}} ->
            unify(BindX, BindY, Bindings, DB)
    end;
unify(X, {var, Y}, Bindings, DB) ->
    case get_binding(Y, Bindings) of
        none ->
            {ok, [{Y, X}|Bindings]};
        {bound, V} ->
            unify(X, V, Bindings, DB)
    end;
unify({var, Y}, X, Bindings, DB) when ?is_primitive(X) ->
    unify(X, {var, Y}, Bindings, DB);
unify(X, X, Bindings, DB) when ?is_primitive(X) ->
    {ok, Bindings};
unify(X, _, _Bindings, _DB) when ?is_primitive(X) ->
    fail;
unify(T1, T2, Bindings, DB) when is_tuple(T1) andalso is_tuple(T2) ->
    if
        size(T1) == size(T2) ->
            unify(tuple_to_list(T1), tuple_to_list(T2), Bindings, DB);
        true ->
            fail
    end;
unify([H1|T1], [H2|T2], Bindings, DB) ->
    case unify(H1, H2, Bindings, DB) of
        {ok, Bind2} ->
            unify(T1, T2, Bind2, DB);
        fail ->
            fail
    end;
unify([], [], Bindings, DB) ->
    {ok, Bindings};
unify(_, _, _, _) ->
    fail.


test_db() ->
    [{rule,liked_by,
      {[{var,'M'},{var,'N'}],[{likes,[{var,'N'},{var,'M'}]}]}},
     {fact,likes,[zoa,sarah]},
     {fact,likes,[robert,sarah]},
     {fact,likes,[zoa,milk]},
     {fact,likes,[robert,cheese]}].



%% @unify_simple(pterm(), pterm(), bindings()) -> {ok, bindings()} | fail
%% @doc First draft, without the database.  Kept around for sanity reasons
%% because it's clean and it appears to work.  A nice reminder now that
%% the db version exists and doesn't work....
unify_simple(X, {var, Y}, Bindings) ->
    case get_binding(Y, Bindings) of
        none ->
            {ok, [{Y, X}|Bindings]};
        {bound, V} ->
            unify_simple(X, V, Bindings)
    end;
unify_simple({var, Y}, X, Bindings) when ?is_primitive(X) ->
    unify_simple(X, {var, Y}, Bindings);
unify_simple(X, X, Bindings) when ?is_primitive(X) ->
    {ok, Bindings};
unify_simple(X, _, _Bindings) when ?is_primitive(X) ->
    fail;
unify_simple(T1, T2, Bindings) when is_tuple(T1) andalso is_tuple(T2) ->
    if
        size(T1) == size(T2) ->
            unify_simple(tuple_to_list(T1), tuple_to_list(T2), Bindings);
        true ->
            fail
    end;
unify_simple([H1|T1], [H2|T2], Bindings) ->
    case unify_simple(H1, H2, Bindings) of
        {ok, Bind2} ->
            unify_simple(T1, T2, Bind2);
        fail ->
            fail
    end;
unify_simple([], [], Bindings) ->
    {ok, Bindings};
unify_simple(_, _, _) ->
    fail.
